FDL - Nuprl Lemma : es-causl-iff

Nuprl Lemma : es-causl-iff

the_es:ES, e, e':E.
(e < e')

first(e') & (e < pred(e'))

e = pred(e')

isrcv(e') & (e < sender(e'))

e = sender(e')

Definitions t T, P Q, x:A. B(x), E, sender(e), (e < e'), P Q, isrcv(e), b, Prop, A & B, pred(e), first(e), A, P Q, P & Q, P Q, ES, (e <loc e'), Trans x,y:T. E(x;y)

Lemmas es-pred-locl, event system wf, es-axioms, not wf, es-first wf, es-pred wf, assert wf, es-isrcv wf, es-causl wf, es-sender wf, es-E wf